ABS: R ||- es.P(es)

STM: R-realizes wf

STM: R-true-rule

STM: R-and-rule

STM: R-none-rule

STM: R-implies-rule

STM: R-all-rule

STM: R-all-rule2

STM: R-and-left

STM: R-init-rule

STM: R-frame-rule

STM: R-sframe-rule

STM: R-aframe-rule

STM: R-bframe-rule

STM: R-rframe-rule

STM: R-effect-rule

STM: R-pre-rule

STM: R-sends-rule

STM: R-usends1-rule

ABS: R-state-var(i;ds;da;x;T;ks;tr)

STM: R-state-var wf

STM: R-state-var-rule

STM: R-state-var-loc

STM: R-state-var-da

STM: R-state-var-da-dom

STM: R-sub-implies

ABS: es.P(es)

STM: es-real wf

ABS: es-realizer(p)

STM: es-realizer wf

STM: implies-es-real

STM: es-real-implies

ABS: es-real-and{i:l}(P;Q;X;Y;p)

STM: es-real-and wf

STM: es-real-monotonicity

STM: init-p-realizable

STM: frame-p-realizable

STM: sframe-p-realizable

STM: effect-p-realizable

STM: pre-p-realizable

STM: discrete-pre-p-realizable

ABS: preinit1R{$x:ut2, $a:ut2}(i; X; p; x0; P)

STM: preinit1R wf

STM: preinit1R feasible

STM: pre-init1-p-realizable

STM: usends1-p-realizable

STM: sends-p-realizable

STM: sends1-p-realizable

STM: conditional-send1-p-realizable

STM: conditional-send-p-realizable

ABS: R-base-recognize(i;ds;x;k;T;test)

STM: R-base-recognize wf

STM: R-base-recognize-realizes2

STM: R-base-recognize-realizes

STM: recognizer-realizable

STM: recognizer-p-realizable

ABS: trigger1{$trigger:ut2, $a:ut2, $x:ut2}(T; A; P; i; k)

STM: trigger1 wf

STM: trigger1 feasible

STM: trigger1-p-realizable

STM: R-state-da-rule

STM: R-compat-state

STM: Reffect-compat

STM: R-compat-base-recognize

STM: not-R-occurs-effect-compat

STM: R-state-var-compat

STM: R-state-var-compat2

STM: R-state-var-compat3

STM: R-state-var-compat-unequal-loc

ABS: R-state-var-init(i;ds;da;x;T;v;ks;tr)

STM: R-state-var-init wf

STM: R-state-var-init-rule

STM: R-state-var-init-compat

STM: sends-p-es-sends-iff

STM: R-lnk-tags-rule

STM: R-state-var-lnk-tags-compat

STM: R-state-var-lnk-tags-compat2

ABS: constR{$x:ut2}(T; c; i)

STM: constR wf

STM: constR feasible

STM: const-realizable

ABS: onceR{$a:ut2, $done:ut2}(i)

STM: onceR wf

STM: onceR feasible

STM: once-realizable

ABS: send_onceR{$done:ut2, $tg:ut2, $b:ut2, $done1:ut2}(T; A; f; l)

STM: send onceR wf

STM: send onceR feasible

STM: send-once-realizable

ABS: at src(l):action $a(m) precondition P sends [$tg,f] on link l

STM: weakPrecondSendR wf

STM: weakPrecondSendR feasible

ABS: weakPrecondSendR2{$a:ut2, $tg:ut2}(T; t; p; l; ds; P; f)

STM: weakPrecondSendR2 wf

STM: weakPrecondSendR2 feasible

STM: weak-precond-send-realizable2

STM: weak-precond-send-realizable

ABS: weakSendDoApplyR{$a:ut2, $tg:ut2}(T; t; l; ds; f)

STM: weakSendDoApplyR wf

STM: weakSendDoApplyR feasible

STM: weak-send-do-apply-realizable

STM: decidable-min-lemma

ABS: sendMinimalR{$a:ut2, $tg:ut2}(T; t; l; ds1; ds2; P; Q; d1; d2; f)

STM: sendMinimalR wf

STM: sendMinimalR feasible

STM: send-minimal-realizable